r:Rng. rxmn  IMonoid 

latex

Up	rings 1
Definitions of Statement	Rng, rxmn
Definitions	rxmn, t  T, x:A. B(x), IMonoid, P & Q, , Mon, P  Q, Rng
Lemmas	rng wf, rng all properties, mon wf, grp id wf, grp op wf, grp car wf, monoid p wf, rng one wf, rng times wf, rng le wf, rng eq wf, rng car wf, mk mon